M:k may not read x
== x  dom(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M))))))))))))
==  deq-member(KindDeq;k;1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M)))))))))))(x)) 

latex

---

clarification:

M:k may not read x
== fpf-dom(IdDeq; x; 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M))))))))))))
==  deq-member(KindDeq;k;fpf-ap(1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(M)))))))))));
==  deq-member(KindDeq;k;fpf-ap(IdDeq;
==  deq-member(KindDeq;k;fpf-ap(x)) 

latex

Definitions	p  q, x  dom(f), b, deq-member(eq;x;L), KindDeq, f(x), 1of(t), 2of(t), IdDeq
FDL editor aliases	ma-no-read